sends k(v:T) on l:
tagged(g,State(ds),v):dt
== (x:Id. vartype(source(l);x)  ds(x)?Top)
== & (e:E. isrcv(e)  lnk(e) = l  valtype(e)  dt(tag(e))?Top)
== & e@source(l).
== & kind(e) = k
== &  valtype(e)  T
== &  & (L:{e:E| isrcv(e) & lnk(e) = l & tag(e)  dom(dt) } List.
== &  & (rcvs from e on l = L
== &  & (& map(e.<tag(e),val(e)>;L)
== &  & (& =
== &  & (& concat(map(tgf.sends-msgs((state when e);val(e);tgf);g))) 

latex

---

clarification:

sends-p(es;ds;k;T;l;dt;g)
== (x:Id. es-vartype(es; source(l); x)  fpf-cap(ds;IdDeq;x;Top))
== & (e:es-E(es).
== & (es-isrcv(es; e)
== & ( es-lnk(es; e) = l  IdLnk
== & ( es-valtype(es; e)  fpf-cap(dt;IdDeq;es-tag(es; e);Top))
== & alle-at(es;source(l);e.es-kind(es; e) = k  Knd
== & alle-at(es;source(l);e. es-valtype(es; e)  T
== & alle-at(es;source(l);e. & (L:{e:es-E(es)
== & alle-at(es;source(l);e. & (L:{| es-isrcv(es; e)
== & alle-at(es;source(l);e. & (L:{| & es-lnk(es; e) = l  IdLnk
== & alle-at(es;source(l);e. & (L:{| & & fpf-dom(IdDeq; es-tag(es; e); dt) } List.
== & alle-at(es;source(l);e. & (es-rcv-from(es;e;l;L)
== & alle-at(es;source(l);e. & (& map(e.<es-tag(es; e),es-val(es; e)>;L)
== & alle-at(es;source(l);e. & (& =
== & alle-at(es;source(l);e. & (& concat(map(tgf.sends-msgs(es-state-when(es;e);es-val
== & alle-at(es;source(l);e. & (& concat(map((es; e);tgf)
== & alle-at(es;source(l);e. & (& concat(map;g))
== & alle-at(es;source(l);e. & (&  (tg:Idfpf-cap(dt;IdDeq;tg;Void)) List)) 

latex

Definitions	sends k(v:T) on l:tagged(g,State(ds),v):dt, vartype(i;x), x:A. B(x), Top, e@i. P(e), source(l), P  Q, Knd, kind(e), valtype(e), x:A. B(x), E, isrcv(e), P & Q, IdLnk, lnk(e), b, x  dom(f), A & B, rcvs from e on l = L, Id, f(x)?z, IdDeq, tag(e), concat(ll), map(f;as), sends-msgs(s;v;tg_f), (state when e), val(e)
FDL editor aliases	sends-p